
\documentclass{IEEEtran}
\usepackage{graphicx}
\usepackage{paralist}
\usepackage{lipsum}
\usepackage{amsmath}
\usepackage{amsfonts}
%\usepackage{natbib}
\usepackage{changebar}
\usepackage{rotating}
\usepackage{amsmath}
\usepackage{mdwlist}
\usepackage{tikz}
%%% algorithm 
\usepackage[linesnumbered]{algorithme} 
\newcommand{\Cla}{\textit{Cla}}
\newcommand{\C}{{\cal C}}
\newcommand{\M}{{\cal M}}
\renewcommand{\L}{{\cal L}}
\renewcommand{\l}{\ell}
\renewcommand{\d}{\delta}
\newcommand{\m}{\mu}
\newcommand{\F}{{\cal F}}
\newcommand{\D}{{\cal D}}
\renewcommand{\S}{{\cal S}}
\newcommand{\ins}{\textit{Ins}}
%% algorithm

%
% in the preamble
%
\newcommand{\specialcell}[2][c]{%
  \begin{tabular}[#1]{@{}c@{}}#2\end{tabular}}
\newcommand{\eat}[1]{}



%opening
\title{Compromising the APDU Layer for Logging into a Smart-card}
\author{Andriana Gkaniatsou\\
a.e.gkaniatsou@sms.ed.ac.uk\\
School Of Informatics,\\
University of Edinburgh,\\
Edinburgh, UK}

\begin{document}

\maketitle

\abstractname{- Formal analysis of security protocols aims to identify possible security vulnerabilities or verify the correctness of such
protocols. A lot of research has focused on developing formal techniques to analyse security protocols, but little attention has been paid to the low-level cryptographic protocols
that implement them. A smart-card or integrated circuit card is advertised as one
of the most secure, tamper-proof, and trusted device for implementing confidential operations such as identification, authentication, data storage and application processing. Such
operations involve the communication between smart-cards
and third-party systems which is defined by the Application Data Unit (APDU). There is an intensive need of a secure implementation of the communication layer, so that sensitive private data are not revealed. Once this layer is compromised, and the implementation is not secure, sensitive data can be available to third-parties and make the smart-card vulnerable to attacks. In this paper we present  REPROVE, a system which analyses a communication trace and produces the list of the exchanged command-response pairs as well as the on-card operations that are executed during this communication. We are particularly interested in the interconnection between the communication layer and the cryptographic functions defined by PKCS\#11, a standard known to be vulnerable to attacks. 
REPROVE does not require access to the card and can analyse both inter-industry and proprietary implementations of the APDU layer. We present our experiments and results on  PKCS\#11 $C\_Log\_In$ the responsible function for logging an application into a token.   }



\section{Introduction}

 Among their many uses, smart-cards are widely used for implementing secure operations, for  private data storage and for communication purposes. 
 A smart-card contains an embedded microprocessor which is responsible for performing cryptographic functions. 
A  smart card has to implement all the cryptographic-relevant operations on the token\footnote{A token is a device that stores objects (data, keys and certificates), which can be accessed via session handles, and  can perform cryptographic functions. } side, \textit{i.e.} on-card.
 The most commonly used cryptographic standard is RSA PKCS\#$11$~\cite{pkcs}, 
which defines an Application Programming Interface (API) for cryptographic devices. It specifies functions such as signing, encryption, decryption, PIN handling, \textit{etc}.  API-related attacks were first introduced in~\cite{Longley} in the early
$1980$s, following the exposure of the vulnerability to attacks of
PKCS \#$11$~\cite{Clulow03onthe, steel10}. Ever since, formally analysing properties of security APIs and reasoning about possible attacks has attracted a lot of attention  \cite{robbank,bakproof,tsalapati, steelxor, steelformalanalysis} and many approaches have been proposed such as using a model checker, a theorem prover, customised decision procedures or reverse-engineering techniques ~\cite{cortier,courant,youn, steelformalanalysis, steel10}.
However, security analysis has mostly focused on the 
PKCS\#$11$ level rather than on implementations closely connected with the standard, such as the low-level communication between the on-card and the off-card applications, 
defined by the Application Data Protocol Unit (APDU).  



A  smart card has to implement all the cryptographic-relevant operations on the token\footnote{A token is a device that stores objects (data, keys and certificates), which can be accessed via session handles, and  can perform cryptographic functions. } side, \textit{i.e.} on-card. The most commonly used cryptographic standard is RSA PKCS\#$11$~\cite{pkcs}, 
which defines an Application Programming Interface (API) for cryptographic devices. It specifies functions such as signing, encryption, decryption, PIN handling, \textit{etc}.  API-related attacks were first introduced in~\cite{Longley} in the early
$1980$s, following the exposure of the vulnerability to attacks of
PKCS \#$11$~\cite{Clulow03onthe, steel10}. Ever since, formally analysing properties of security APIs and reasoning about possible attacks has attracted a lot of attention  \cite{robbank,bakproof,tsalapati, steelxor, steelformalanalysis} and many approaches have been proposed such as using a model checker, a theorem prover, customised decision procedures or reverse-engineering techniques ~\cite{cortier,courant,youn, steelformalanalysis, steel10}.
However, security analysis has mostly focused on the 
PKCS\#$11$ level rather than on implementations closely connected with the standard, such as the low-level communication between the on-card and the off-card applications, 
defined by the Application Data Protocol Unit (APDU).  
The pin configuration of a smart-card is defined by ISO 7816-2 while all communication to the card is via a single input-output line, using a linear communication protocol. The higher-level communication (APDU layer), 
the commands and the rules that govern APDU layer are defined by ISO 7816-4, e.g., the available 
inter-industry commands, the structure and contents of the exchanged messages \textit{etc}. It is up to the card manufacturer whether the implementation 
of the ISO itself will be either inter-industry or proprietary.



%%Smart Card Attacks
As it is very often that sensitive data is stored on-card, e.g, a cryptographic key , a PIN, an authentication certificate, \textit{e.t.c.}, such data should be kept secret 
to prevent counterfeiting of a card, or attacking a system't security. Exploiting sensitive data linkage on smart-cards is not a novel idea, with side channel attacks by exploiting the power 
consumption eg., \cite{kocher1999},  to attract a lot of attention. In our work we are concerned with sensitive data linkage at the APDU layer.
If an attacker compromises that layer and the communication is not implemented in a secure way, he can have access to the card's operations and consequently to sensitive information, 
\textit{eg.}, keys  or data that should be encrypted but is not.  \cite{Murdoch-chp-PIN}, for instance,  proposes  a man-in-the-middle device to allow authentication without knowing the card's PIN. 
The proposed  system intercepts and modifies the communication between the card and the terminal. Under the assumption that APDUs are inter-industry, it sends a $success$ response to a $verify$ command that 
has the wrong PIN and  allows authentication of untrustworthy parts. In \cite{barbu-eavesdropPINg-apdu-buffer} a different approach is adopted: the bypassing of the confidentiality insurance under the assumption 
that an attacker has access to the APDU buffer\footnote{The buffer that  is used to exchange data.}. \cite{smartlogig-koning} presents the SmartLogic tool which  provides full control over the smart-card  
communication channel for eavesdropping and man-in-the-middle attacks. The smart-card communication channel has to be implemented in an inter-industry way for SmartLogic to be successful.  
All these efforts to prove security vulnerabilities of the smart-cards create the need to define a formal way of analysing and reasoning about their security. The above approaches deal only 
with inter-industry implementations whereas proprietary ones should also be considered as they are very common. In proprietary commands what aggravates the situation is that they effectively 
look like a random sequence of bits that we need to decipher in order to understand their semantics.

In this paper we present REPROVE, a system for automatically analysing  APDU traces. 
 REPROVE takes as input an APDU trace 
reverse-engineers  the semantics of it, and infers the interconnection with the PKCS\#11 functions. The output of the analysis is a list of the command-response pairs that were exchanged and a list of card operations that we executed during the communication. The difference of REPROVE and already existing reverse-engineering engines for protocols is that REPROVE does not require access to the card, as it also assumes unknown semantics of the implementation. 
\eat{A lot of research has been conducted in the protocol reverse-engineering research area. }
For instance,  the Polygot system \cite{polygot} automatically extracts protocol messages through binary analysis, the Prospex system \cite{prospex}  
infers the protocol format and the corresponding state machines.  \cite{reformat} presents ReFormat, a system  for reverse-engineering encrypted messages. \cite{cho2010} proposes 
the inference of  protocol state machines based on abstractions that the end users provide.  None of these methodologies suit to our problem as we assume that we cannot  access the card, unknown message semantics (proprietary implementations), and we also target the interconnection between the 
communication and the  PKCS\#11 itself.
 
 
 
 
 
 We tested REPROVE in five commercially available smart-cards and the results are encouraging. In this document we present the results.

We test REPROVE system for the $C\_LogIn$ RSA PKCS \# 11 function.

\subsection{PKCS\# C$\_$LogIn}
When an application connects to the token it initiates a session. Sessions can be public or private.  $C\_LogIn$ is the responsible function for logging into the token an application (a user or a Security Officer \textbf{SO}). An application can login to a private session only if the $C\_LogIn$ application has been called successfully.  
  The type of session defines the type of objects the application can access and perform operations. The sessions are also categorised depending on the operations the application can perform to Read-Only and Read-Write. The objects that the application has access also depends on the session type: public or private objects. An application can change session type \textit{e.g.,} public $\rightarrow$ private by logging in successfully, and vice versa.   
Table~\ref{sessionTypes} presents the sessions and transitions that PKCS \# 11 defines.


\begin{table}[h!]
  \centering
  \begin{tabular}{| c | c | c|  }
\hline
Session Type & Log-In & Operations \\
\hline
Public &  no &Read Only\\
 Private & yes & Read Only \\
 Public  & no & Read-Write\\
 Private & yes & User Read-Write\\
 Private & yes & SO Read-Write \\
\hline
\end{tabular}
   \caption{Cryptoki Session Types}
  \label{sessionTypes}
\end{table}


\paragraph{C$\_LogIn$ Properties}PKCS\#11 states that all sessions that an application has with a token must have the same state \textit{i.e.} if a session is logged in then all other sessions are also logged in. If a session deals with private keys, the corresponding operations can only be executed if  C$\_$LogIn is called successfully. A similar approach is used for the flags, where the flag $CKF\_Write\_Protected$ is true unless $C\_LogIn$ is true. 

\subsection{C$\_$LogIn Security Vulnerabilities}
The outcome of the analysis is a model that suggests of how the card implements this specific cryptographic function at the communication layer. From this model we 
can infer specific security properties or vulnerabilities of the design of this protocol. In particular, depending on the implementation we can draw our attention on the 
different security aspects. 
\paragraph{Log$\_$in bypass attacks} If the protocol allows the attacker to understand the implementation of this specific function, there are several ways that one may bypass it. For instance, looping the session while the logging in takes place and taking advantage the active authentication of all other sessions. In this way, one can initiate another session to manipulate private data. After the desired operations have taken place, the logging in session can be closed. 
\paragraph{Knowledge of the PIN} If the implementation of this function allows the PIN to be sent plaintext, one can easily sniff it and use it whenever and for any purpose that he likes, for instance blind reply the sessions.  
\paragraph{Brute force PIN attack}


We tested the analysis system for the $log\_in$ function in 5 smart-cards. Tables 1-5 present the 
results of our system. A \textit{combination} also represents a search path. 
\textit{Total command combinations} represents all possible combinations that can be made without any restrictions (abstract models, preconditions etc.), \textit{valid command combinations} stands for the command combinations that we consider valid based on the abstract models, \textit{sub-functionality combinations} and \textit{functionality combinations} represent all possible such combinations. \textit{PKCS models} refers to the resulted suggestions of how the card implements this specific cryptographic function. 

\textbf{Safesite Classic TPC IS V1} The trace consists of two commands. The results we obtained are presented in Table~\ref{safesite}. The resulted model matches exactly with the original implementation.

\begin{table}[position specifier]
  \centering
  \begin{tabular}{| l | c |  }
\hline
Analysis Level & Results \\
\hline
Total Command Combinations &  1\\
 Valid Command Combinations &  1 \\
 Sub-Functionality Combinations  & 1\\
 Functionality Combinations &  1\\
 PKCS Models & 1 \\
\hline
\end{tabular}
   \caption{Safesite Classic TPC IS V1}
  \label{safesite}
\end{table}


\textbf{Siemens CardOS V4.3b} The trace consists of two commands. The results we obtained are presented in Table~\ref{siemens}. The resulted model matches exactly with the original implementation.


\begin{table}[position specifier]
  \centering
  \begin{tabular}{| l | c |  }
\hline
Analysis Level & Results \\
\hline
Total Command Combinations & 1 \\
 Valid Command Combinations & 1 \\
 Sub-Functionality Combinations  &1 \\
 Functionality Combinations & 1\\
 PKCS Models & 1\\
 \hline
\end{tabular}
   \caption{Siemens CardOS V4.3b}
  \label{siemens}
\end{table}





\textbf{Aladdin eToken PRO} The trace consists of 5 commands. The results we obtained are presented in Table~\ref{aladdin}. The system suggested 2 possible implementations of the $log\_in$ function: both of the same abstraction. 1/2 models matches exactly with the original implementation.

\begin{table}[position specifier]
  \centering
  \begin{tabular}{| l | c |  }
\hline
Analysis Level & Results \\
\hline
Total Command Combinations & 104 \\
 Valid Command Combinations & 6 \\
 Sub-Functionality Combinations  & 4\\
 Functionality Combinations & 3\\
 PKCS Models & 2\\
\hline 
\end{tabular}
   \caption{Aladdin eToken PRO}
  \label{aladdin}
\end{table}




\textbf{Athena ASEKey USB} The trace consists of 13 commands. The results we obtained are shown in Table~\ref{athena}. The system suggested 3 possible implementations of the $log\_in$ function, all of the same abstraction. 1/3 matches exactly with the actual implementation (I think there is a possibility that another one is correct(!) - need to discuss this).


\begin{table}[position specifier]
  \centering
  \begin{tabular}{| l | c |  }
\hline
Analysis Level & Results \\
\hline
Total Command Combinations &  73651\\
 Valid Command Combinations &  8 \\
 Sub-Functionality Combinations  & 6\\
 Functionality Combinations & 3 \\
 PKCS Models & 3 \\
\hline 
\end{tabular}
   \caption{Athena ASEKey USB}
  \label{athena}
\end{table}



\textbf{RSA SecurID 800} The trace consists of 3 commands. The results we obtained are presented in Table~\ref{rsa}. The system suggested 1 model which matches exactly with the original implementation/


\begin{table}[position specifier]
  \centering
  \begin{tabular}{| l | c |  }
\hline
Analysis Level & Results \\
\hline
Total Command Combinations & 222\\
 Valid Command Combinations &  51\\
 Sub-Functionality Combinations  & 33\\
 Functionality Combinations & 4\\
 PKCS Models & 1\\


\hline 
\end{tabular}
   \caption{RSA SecurID 800}
  \label{rsa}
\end{table}



\bibliographystyle{abbrv}
\bibliography{references}


\end{document}
